\begin{tabbing}
$\forall$$T$:Type, ${\it eq}$, $r$:($T$$\rightarrow$$T$$\rightarrow\mathbb{B}$).
\\[0ex]($\forall$$a$, $b$:$T$. ($\uparrow$(${\it eq}$($a$,$b$))) $\Leftarrow\!\Rightarrow$ ($a$ = $b$))
\\[0ex]$\Rightarrow$ Linorder($T$;$a$,$b$.$\uparrow$($r$($a$,$b$)))
\\[0ex]$\Rightarrow$ \=($\forall$$x$:$T$, $L$:($T$ List).\+
\\[0ex]sorted{-}by($\lambda$$x$,$y$. $\uparrow$($r$($x$,$y$));$L$) $\Rightarrow$ no\_repeats($T$;$L$) $\Rightarrow$ no\_repeats($T$;insert{-}by(${\it eq}$;$r$;$x$;$L$)))
\-
\end{tabbing}